Commit Graph

390 Commits (f2cd03a11e025343471636e7108112bd316b748e)

Author SHA1 Message Date
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 5 years ago
Josh Berdine 429fbddeda [sledge] Refine inlining heuristic to allow casts 5 years ago
Josh Berdine d6d65a785a [sledge] Remove left-over SSA assertion 5 years ago
Josh Berdine 7105d85281 [sledge][NFC] Minor code cleanup 5 years ago
Josh Berdine 081455278d [sledge] Do not explore exceptional control flow by default 5 years ago
Josh Berdine 9acfb65ba0 [sledge][NFC] Update TODO 5 years ago
Josh Berdine bc858fad2e [sledge][NFC] Rename Term.call's func arg to callee to match type 5 years ago
Josh Berdine 6399c59861 [sledge] Do not represent function CFGs explicitly 5 years ago
Josh Berdine 2331e8d68a [sledge] Fix frontend bug in trampoline creation 5 years ago
Josh Berdine cf5097a8b4 [sledge] Add report-summary test make target 5 years ago
Josh Berdine 995de071ed [sledge] Revise Sh_domain handling of function call and return 5 years ago
Josh Berdine df26b9b1a5 [sledge][NFC] Minor code simplification 5 years ago
Josh Berdine 65e963a162 [sledge] Add Sh.subst implemented ito and and exists 5 years ago
Josh Berdine 1595fb7c60 [sledge] Fix potential name clash in Sh.rename 5 years ago
Josh Berdine 799b21761f [sledge] Translate ExtractElement and InsertElement despite being vector 5 years ago
Scott Owens 3080fba8fa [sledge sem] Update LLVM and LLAIR sem for consistent stuckness 5 years ago
Scott Owens 14a8ae34b9 [sledge sem] Improve and unify treatment of Exit 5 years ago
Scott Owens 5312b3d10c [sledge sem] Fix trans. invariant for llair expressions 5 years ago
Scott Owens 9f2f14b34c [sledge sem] Sketch out translation correctness 5 years ago
Jules Villard 42470d8809 [hmm] sexp_{option,list} -> {option,list} 5 years ago
Josh Berdine ef78ba83cf [sledge] Report the number of alarms 5 years ago
Josh Berdine ec52c05c30 [sledge][NFC] Minor simplification for singleton sets 5 years ago
Josh Berdine 239d906ab6 [sledge] Improve tracing and debugging support 5 years ago
Josh Berdine 3f5adecdcf [sledge] Exec.exec_specs missed vocabulary extension 5 years ago
Josh Berdine 9ac854c970 [sledge] Exec.kill should preserve vocabulary 5 years ago
Josh Berdine 8097f1a6df [sledge] Adjust tests to match harnesses 5 years ago
Josh Berdine b2f90a3994 [sledge] Treat freturn directly in Dom.call 5 years ago
Josh Berdine fbf0fe2f1a [sledge][NFC] Rename args to actuals 5 years ago
Josh Berdine d3d0c4b36e [sledge][NFC] Rename params to formals 5 years ago
Josh Berdine 69c29ab3d8 [sledge][NFC] Label args of Domain.call 5 years ago
Josh Berdine 47766a0e6e [sledge] Drop globals with appending linkage and size 0 5 years ago
Josh Berdine 1efd0df035 [sledge] Avoid potential name clash between trampolines 5 years ago
Josh Berdine ebee451f1c [sledge] Improve test scripts 5 years ago
Josh Berdine 38cab376f6 [sledge] Keep BitCasts and similar in expressions 5 years ago
Josh Berdine b632d4f283 [sledge] Check the input datalayout agrees with assumptions 5 years ago
Josh Berdine 6328a6ce40 [sledge] Do not store size of globals separately 5 years ago
Josh Berdine ca95fc098f [sledge] Keep size in both bits and bytes for each type 5 years ago
Josh Berdine d3bad1ce44 [sledge] Add sizes to types 5 years ago
Josh Berdine 6120b7d098 [sledge] Use the configured margin when formatting failure messages 5 years ago
Josh Berdine a386b36616 [sledge] Re-add Splat expression for zero-initialized aggregates 5 years ago
Josh Berdine 727385d853 [sledge] Relax Typ.is_sized to allow opaque types 5 years ago