Commit Graph

392 Commits (773766e3f70c2b753613b8c5bde09685679f261d)

Author SHA1 Message Date
Scott Owens f68258ca73 [sledge sem] Update sanity proof for LLAIR convert 5 years ago
Benno Stein beb99932c3 [sledge] Handle more LLAIR expressions in APRON interval analysis 5 years ago
Josh Berdine 752b8ab56a [sledge] Fix normalization of Convert terms 5 years ago
Scott Owens 5caa19990b [sledge sem] Improve a comment 5 years ago
Scott Owens a4f0d6dbb7 [sledge sem] Complete (nearly) proof for phi instrs 5 years ago
Benno Stein 50b60bc049 [sledge] Add APRON-backed Interval abstract domain 5 years ago
Scott Owens 9f0fdd3bfe [sledge sem] Add proof of bit cast implementation 5 years ago
Scott Owens e9296d31b6 [sledge sem] Implement and verify cast expressions 5 years ago
Scott Owens 86024892e1 [sledge sem] Refactor inductive definitions a bit 5 years ago
Scott Owens 573f0d8aed [sledge sem] Make proof progress on phi instructions 5 years ago
Scott Owens 0a35b1da35 [sledge sem] Prove the Load and Store cases (mostly) 5 years ago
Josh Berdine c0c96b5235 [sledge] Refactor Used globals analysis results type and query 6 years ago
Josh Berdine 429fbddeda [sledge] Refine inlining heuristic to allow casts 6 years ago
Josh Berdine d6d65a785a [sledge] Remove left-over SSA assertion 6 years ago
Josh Berdine 7105d85281 [sledge][NFC] Minor code cleanup 6 years ago
Josh Berdine 081455278d [sledge] Do not explore exceptional control flow by default 6 years ago
Josh Berdine 9acfb65ba0 [sledge][NFC] Update TODO 6 years ago
Josh Berdine bc858fad2e [sledge][NFC] Rename Term.call's func arg to callee to match type 6 years ago
Josh Berdine 6399c59861 [sledge] Do not represent function CFGs explicitly 6 years ago
Josh Berdine 2331e8d68a [sledge] Fix frontend bug in trampoline creation 6 years ago
Josh Berdine cf5097a8b4 [sledge] Add report-summary test make target 6 years ago
Josh Berdine 995de071ed [sledge] Revise Sh_domain handling of function call and return 6 years ago
Josh Berdine df26b9b1a5 [sledge][NFC] Minor code simplification 6 years ago
Josh Berdine 65e963a162 [sledge] Add Sh.subst implemented ito and and exists 6 years ago
Josh Berdine 1595fb7c60 [sledge] Fix potential name clash in Sh.rename 6 years ago
Josh Berdine 799b21761f [sledge] Translate ExtractElement and InsertElement despite being vector 6 years ago
Scott Owens 3080fba8fa [sledge sem] Update LLVM and LLAIR sem for consistent stuckness 6 years ago
Scott Owens 14a8ae34b9 [sledge sem] Improve and unify treatment of Exit 6 years ago
Scott Owens 5312b3d10c [sledge sem] Fix trans. invariant for llair expressions 6 years ago
Scott Owens 9f2f14b34c [sledge sem] Sketch out translation correctness 6 years ago
Jules Villard 42470d8809 [hmm] sexp_{option,list} -> {option,list} 6 years ago
Josh Berdine ef78ba83cf [sledge] Report the number of alarms 6 years ago
Josh Berdine ec52c05c30 [sledge][NFC] Minor simplification for singleton sets 6 years ago
Josh Berdine 239d906ab6 [sledge] Improve tracing and debugging support 6 years ago
Josh Berdine 3f5adecdcf [sledge] Exec.exec_specs missed vocabulary extension 6 years ago
Josh Berdine 9ac854c970 [sledge] Exec.kill should preserve vocabulary 6 years ago
Josh Berdine 8097f1a6df [sledge] Adjust tests to match harnesses 6 years ago
Josh Berdine b2f90a3994 [sledge] Treat freturn directly in Dom.call 6 years ago
Josh Berdine fbf0fe2f1a [sledge][NFC] Rename args to actuals 6 years ago
Josh Berdine d3d0c4b36e [sledge][NFC] Rename params to formals 6 years ago
Josh Berdine 69c29ab3d8 [sledge][NFC] Label args of Domain.call 6 years ago
Josh Berdine 47766a0e6e [sledge] Drop globals with appending linkage and size 0 6 years ago
Josh Berdine 1efd0df035 [sledge] Avoid potential name clash between trampolines 6 years ago
Josh Berdine ebee451f1c [sledge] Improve test scripts 6 years ago
Josh Berdine 38cab376f6 [sledge] Keep BitCasts and similar in expressions 6 years ago
Josh Berdine b632d4f283 [sledge] Check the input datalayout agrees with assumptions 6 years ago
Josh Berdine 6328a6ce40 [sledge] Do not store size of globals separately 6 years ago
Josh Berdine ca95fc098f [sledge] Keep size in both bits and bytes for each type 6 years ago
Josh Berdine d3bad1ce44 [sledge] Add sizes to types 6 years ago
Josh Berdine 6120b7d098 [sledge] Use the configured margin when formatting failure messages 6 years ago