diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-27 10:04:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-27 10:04:42 +0100 |
| commit | 0d389125f75cfeaa29850679acf3a20bc8662afa (patch) | |
| tree | 6ce8869aed0e79911405a03e6c430dc93ef14fbb /backend | |
| parent | 8eefcaadda8d0fb81e2f3c81bb5e0586b8f69585 (diff) | |
| download | compcert-kvx-0d389125f75cfeaa29850679acf3a20bc8662afa.tar.gz compcert-kvx-0d389125f75cfeaa29850679acf3a20bc8662afa.zip | |
invariant printing more aligned with RTL dumps
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE3analysisaux.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/CSE3analysisaux.ml b/backend/CSE3analysisaux.ml index 1385b3d3..8c83dc2e 100644 --- a/backend/CSE3analysisaux.ml +++ b/backend/CSE3analysisaux.ml @@ -88,7 +88,7 @@ let pp_equation hints chan x = print_eq chan (P.to_int eq.eq_lhs, eq.eq_op, List.map P.to_int eq.eq_args);; let pp_relation hints chan rel = - pp_set ", " (pp_equation hints) chan rel;; + pp_set "; " (pp_equation hints) chan rel;; let pp_relation_b hints chan = function | None -> output_string chan "bot" @@ -96,7 +96,7 @@ let pp_relation_b hints chan = function let pp_results f (invariants : RB.t PMap.t) hints chan = let max_pc = P.to_int (RTL.max_pc_function f) in - for pc=1 to max_pc + for pc=max_pc downto 1 do Printf.fprintf chan "%d: %a\n" pc (pp_relation_b hints) (PMap.get (P.of_int pc) invariants) |