Commits

Commits on Dec 21, 2021

Export more constructors to enable mem log analysis

travitch
authored and
robdockins
committedDec 21, 2021
Make an internal memory model module accessible

travitch
authored and
robdockins
committedDec 21, 2021

Commits on Jan 30, 2021

Add some extra documentation on Crucible backends
travitch
committedJan 30, 2021

Commits on Dec 18, 2020

crucible-llvm: Add another test for the SMT array memory model
travitch
committedDec 18, 2020

Commits on Dec 17, 2020

Make the crucible-llvm tests more configurable
travitch
committedDec 17, 2020

Commits on Oct 29, 2020

fixpoint: Export additional types and functions to make the modified interface usable
travitch
committedOct 29, 2020

Commits on Oct 7, 2020

Get the crucible-llvm tests compiling again
travitch
committedOct 7, 2020
Update the crucible tests to account for an extra type parameter
travitch
committedOct 7, 2020

Commits on Jun 16, 2020

Add some documentation about the 'HasModel' constraint
travitch
committedJun 16, 2020
Merge remote-tracking branch 'origin' into tr/crux-personality
travitch
committedJun 16, 2020
Generalize crux to allow clients to use their own personality type
travitch
committedJun 16, 2020

Commits on Apr 17, 2020

Add a bit of documentation on the LLVM memory model
travitch
committedApr 17, 2020

Commits on Feb 5, 2020

Fix a haddock error
travitch
committedFeb 5, 2020

Commits on Feb 4, 2020

crux: Eliminate the yices/unsat core warning for offline solving
travitch
committedFeb 4, 2020
crux: Use a record type to track proved/disproved goals
travitch
committedFeb 4, 2020

Commits on Feb 2, 2020

what4: Another dReal adapter fix
travitch
committedFeb 2, 2020

Commits on Feb 1, 2020

crux: Respect per-goal timeouts in the offline proving backend
travitch
committedFeb 1, 2020

Commits on Jan 31, 2020

Commits on Jan 30, 2020

crux: Allow independent selection of solvers for pathsat checking and goal solving
travitch
committedJan 30, 2020

Commits on Jan 14, 2020

Fix(?) online solver process termination
travitch
committedJan 14, 2020

Commits on Dec 30, 2019

Improve the SMT generated for array lookups with symbolic indices

travitch
authored and
robdockins
committedDec 30, 2019

Commits on Aug 29, 2019

Clang generates vectorized comparisons that we need to be able to handle

travitch
authored and
robdockins
committedAug 29, 2019

Commits on Jul 25, 2019

Add a special case to the memory model to load 0 at pointer types
travitch
committedJul 25, 2019

Commits on May 28, 2019

Fix the extern "C" preprocessor guards in crucible.h for crux
travitch
committedMay 28, 2019
Use arrayUpdate to reduce the number of memory writes
travitch
committedMay 28, 2019
Make symbolic strings mutable
travitch
committedMay 28, 2019

Commits on May 24, 2019

Add an extra test for crucible_string
travitch
committedMay 24, 2019
Add a crux primitive: crucible_string
travitch
committedMay 24, 2019

Commits on May 21, 2019

what4: Fix SMT generation for z3 in the presence of exists/forall pro… (#235 )

travitch
authored and
robdockins
committedMay 21, 2019

Commits on May 20, 2019

what4: Explicitly shut down the solver connection for yices
travitch
committedMay 20, 2019

Commits on Jan 12, 2019

Expose Lang.Crucible.LLVM.UndefinedBehavior
travitch
committedJan 12, 2019

Commits on Aug 9, 2018

Avoid dividing by zero while simplifying expressions
travitch
committedAug 9, 2018