Code

Simple loop invariants#1725

Code

Merged

mergify[bot] merged 12 commits intomasterGaloisInc/saw-script:masterfrom rwd/simple-loop-invariantGaloisInc/saw-script:rwd/simple-loop-invariantCopy head branch name to clipboardSep 19, 2022

+198-9

Commits

Commits on Sep 19, 2022

• bump crucible to current master

  

  robdockins

  authored and

  RyanGlScott

  committed
  3a64f77

• WIP, install the new loop fixpoint feature

  

  robdockins

  authored and

  RyanGlScott

  committed
  4042b53

• Tweaks to the simple loop fixpoint2 feature

  

  robdockins

  authored and

  RyanGlScott

  committed
  8157e0f

• Add tags to goals resulting from the loop invariant feature.

  Show description for 7a45455
  

  robdockins

  authored and

  RyanGlScott

  committed
  7a45455

• Pipe in the additional integer argument for the loop invariant feature.

  Show description for 9d8daac
  

  robdockins

  authored and

  RyanGlScott

  committed
  9d8daac

• Rename the functions binding to the new simple loop invariant feature.

  

  robdockins

  authored and

  RyanGlScott

  committed
  de47099

• Better output handling for the simple loop invariant feature.

  Show description for 0ee1eda
  

  robdockins

  authored and

  RyanGlScott

  committed
  0ee1eda

• Apply suggestions from code review

  Show description for 2867e1d
  

  robdockins

  and

  RyanGlScott

  committed
  2867e1d

• More extensive help documentation for llvm_verify_x86_with_invariant.

  

  robdockins

  authored and

  RyanGlScott

  committed
  00d9ba3

• Additional comments

  

  robdockins

  authored and

  RyanGlScott

  committed
  71f15ad

• typo, improved helpstring

  

  robdockins

  authored and

  RyanGlScott

  committed
  207b068

• update changelog

  

  robdockins

  authored and

  RyanGlScott

  committed
  37e9f97