21 Commits

Author	SHA1	Message	Date
Leo Alt	8d91ccf028	[SMTChecker] Add a new trusted mode which assumes that code that is ... available at compile time is trusted.	2023-02-06 17:02:33 +01:00
Leo Alt	9bcd2c18e4	Add expression substitution to Predicate	2021-10-26 11:30:30 +02:00
Leo Alt	4c2b661eaa	[SMTChecker] Report values for block, msg and tx variables in counterexamples	2021-10-05 15:19:10 +02:00
chriseth	e3525b81d0	Supply scanner to model checker.	2021-07-14 15:12:10 +02:00
Leonardo Alt	ba97d6ac4e	Add local vars to cex	2021-03-30 17:55:21 +02:00
Mathias Baumann	e197ebbdd1	Replace TypePointer with Type const*	2021-03-23 11:47:19 +01:00
Leonardo Alt	665ce27c18	Fix inheritance bug in CHC cex	2021-02-02 18:06:32 +01:00
Leonardo Alt	a612daa783	Add msgvalue to cex	2021-01-21 19:05:44 +01:00
Leonardo Alt	007d39871b	[SMTChecker] Synthesize untrusted functions called externally	2021-01-15 11:56:26 +01:00
Leonardo Alt	b3c3836388	Output internal calls	2021-01-12 14:57:04 +01:00
Leonardo Alt	11f56861c3	Refactor cex loop	2021-01-07 23:13:02 +01:00
Leonardo Alt	b7ac207391	[SMTChecker] Support return in CHC	2020-12-07 18:17:33 +01:00
Leonardo Alt	7490ffbe13	Use nonlinear clauses instead of inlining for base constructors	2020-12-04 13:25:56 +01:00
Leonardo Alt	f2f84a7f97	Format array cex	2020-10-27 16:32:43 +00:00
Leonardo Alt	446e46fe06	Use Expression instead of plain strings for counterexamples	2020-10-27 12:04:51 +00:00
Leonardo Alt	c8cc73c80c	Support array slices	2020-10-01 11:52:02 +02:00
Leonardo Alt	3519b38055	Move predicate functions from CHC to PredicateInstance	2020-09-28 12:43:19 +02:00
Leonardo Alt	a3b6019131	Move post input and post output filtering from CHC to Predicate	2020-09-01 16:10:12 +02:00
Leonardo Alt	2e2e96cc93	Move state model filtering from CHC to Predicate	2020-09-01 16:10:12 +02:00
Leonardo Alt	e3a8c94ace	Move formatFunctionCallCounterexample from CHC to Predicate	2020-09-01 16:10:11 +02:00
Leonardo Alt	016b9b83a8	Refactor predicates	2020-09-01 16:09:56 +02:00