Skip to content

Commit

Permalink
fix(pv): fix locally a division by zero occuring in Proverif
Browse files Browse the repository at this point in the history
This division by zero occurs when proverif is ran from a non-TTY.
  • Loading branch information
W95Psp committed Oct 24, 2024
1 parent 9331cec commit d5ed286
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 1 deletion.
7 changes: 6 additions & 1 deletion examples/default.nix
Original file line number Diff line number Diff line change
Expand Up @@ -47,5 +47,10 @@ in
sed -i "s/make -C limited-order-book/HAX_VANILLA_RUSTC=never make -C limited-order-book/g" Makefile
make
'';
buildInputs = [hax hax-env fstar jq proverif];
buildInputs = [
hax hax-env fstar jq
(proverif.overrideDerivation (_: {
patches = [ ./proverif-psk/pv_div_by_zero_fix.diff ];
}))
];
})
13 changes: 13 additions & 0 deletions examples/proverif-psk/pv_div_by_zero_fix.diff
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
diff proverif2.05/src/display.ml proverif2.05/src/display.ml
index c43785ec..2763d907 100644
--- proverif/src/display.ml
+++ proverif/src/display.ml
@@ -49,7 +49,7 @@ let dynamic_display str =
then display_whitespace (!record_cursor_line - size);
(* If we cannot determine the number of columns, we just assume that the statistics
will fit on one line (the statistics will not be active by default) *)
- let lines = if columns = -1 then 0 else ((max (!record_cursor_line) size) - 1) / columns in
+ let lines = if columns <= 0 then 0 else ((max (!record_cursor_line) size) - 1) / columns in
(* Go to the beginning of the line *)
print_string "\r";
if lines > 0 then

0 comments on commit d5ed286

Please sign in to comment.