Store domain and its value in summary

diffblue / 2ls

Static Analyzer and Verifier

http://www.cprover.org/2LS

Other

43 stars 22 forks source link

Store domain and its value in summary #144

Closed FrNecas closed 3 years ago

FrNecas commented 3 years ago

This is a preparation for implementation of GOTO code instrumentation. It will be useful to have access to the whole domain to be able to easily instrument GOTO code with invariants. It was necessary to slightly tweak how summary_db works with summaries (previously, summaries were copied when obtaining them from summary_db, references are returned after the changes).

viktormalik commented 3 years ago

@viktormalik,I guess this should wait until you've merged your SV-COMP fixes?

There shouldn't be any conflict but I agree, let's merge the SV-COMP fixes first (PR is open already) so that we can tag the exact version that was used in SV-COMP and then proceed with this.