Correctly extract dummy instr_info to 1 (one)

Fixes #224
jasmin-lang · Aug 31, 2022 · 370a83f · 370a83f
1 parent 8c18e43
commit 370a83f
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -25,6 +25,10 @@
   ([PR #216](https://github.com/jasmin-lang/jasmin/pull/216);
   fixes [#200](https://github.com/jasmin-lang/jasmin/issues/200)).
 
+- Do not spuriously warn about missing “iinfo”
+  ([PR #225](https://github.com/jasmin-lang/jasmin/pull/225);
+  fixes [#224](https://github.com/jasmin-lang/jasmin/issues/224)).
+
 ## New features
 
 - Fill an array with “random” data using `p = #randombytes(p);`

diff --git a/compiler/tests/success/bug_224.jazz b/compiler/tests/success/bug_224.jazz
@@ -0,0 +1,6 @@
+export
+fn main(reg u64 x) {
+  while {
+    x -= 1;
+  } (x > 0)
+}
diff --git a/proofs/lang/extraction.v b/proofs/lang/extraction.v
@@ -23,7 +23,7 @@ Extract Constant expr.VarInfo.t => "Location.t".
 Extract Constant expr.VarInfo.witness => "Location._dummy".
 Extract Constant expr.var_info => "Location.t".
 Extract Constant expr.InstrInfo.t => "Stdlib.Int.t".
-Extract Constant expr.InstrInfo.witness => "(-1)".
+Extract Constant expr.InstrInfo.witness => "1".
 Extract Constant expr.instr_info => "Stdlib.Int.t".
 
 Cd  "lang/ocaml".