32 Commits

Author	SHA1	Message	Date
Tyler	519e1c9402	Specify namespaces ... Fix references into solidity::util	2022-03-08 00:09:17 -05: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
Leo Alt	e74f853c6b	[SMTChecker] Support user types	2021-09-21 13:23:17 +02:00
chriseth	90c4623460	Some more base fees.	2021-08-12 16:37:21 +02:00
chriseth	e3525b81d0	Supply scanner to model checker.	2021-07-14 15:12:10 +02:00
chriseth	f75b55071e	Remove CharStream from SourceLocation.	2021-07-14 15:12:07 +02:00
Leonardo Alt	4e34359063	Basic support to free functions	2021-04-19 19:23:18 +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	b02722ebda	Add contract name to called function in cex	2021-01-04 10:03:16 +01:00
Leonardo Alt	2cbf33ca1c	SMTChecker support ABI functions as UFs	2020-12-17 14:03:17 +01:00
Martin Blicha	eb356735f6	[SMTChecker] Adding support for reporting values of structs in CEX in CHC engine.	2020-12-08 16:40:28 +01:00
Leonardo Alt	7490ffbe13	Use nonlinear clauses instead of inlining for base constructors	2020-12-04 13:25:56 +01:00
Alex Beregszaszi	2f899bbffa	[SMTChecker] Avoid implicit conversion	2020-11-11 16:29:03 +00:00
Leonardo Alt	25f75ce547	Remove nondet tests	2020-10-28 11:03:42 +00: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	54f76e081a	[SMTChecker] Support crypto functions in CHC	2020-10-16 14:57:13 +01:00
Leonardo Alt	440e5b3935	[SMTChecker] Fix counterexample state reporting	2020-10-13 22:18:43 +01:00
Leonardo Alt	aec456021d	Add tx constraints to CHC	2020-10-13 17:49:04 +01:00
Leonardo Alt	18cf01c187	Add this and state to CHC	2020-10-12 11:11:52 +01: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