Merge pull request #521 from pq-code-package/cbmc-counter-not-line

hanno-becker · web-flow · commit 614529e48b35 · 2025-10-02T19:43:32.000+01:00
Use COUNTER instead of LINE for quantified variables
diff --git a/mldsa/cbmc.h b/mldsa/cbmc.h
@@ -126,7 +126,7 @@
   }
 
 #define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \
-  array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb),      \
+  array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb),      \
       (qvar_ub), (array_var), (value_lb), (value_ub))
 /* clang-format on */
 

Original file line number	Diff line number	Diff line change
`@@ -126,7 +126,7 @@`
`126`	`126`	`}`
`127`	`127`
`128`	`128`	`#define array_bound(array_var, qvar_lb, qvar_ub, value_lb, value_ub) \`
`129`		`- array_bound_core(CBMC_CONCAT(_cbmc_idx, __LINE__), (qvar_lb), \`
	`129`	`+ array_bound_core(CBMC_CONCAT(_cbmc_idx, __COUNTER__), (qvar_lb), \`
`130`	`130`	`(qvar_ub), (array_var), (value_lb), (value_ub))`
`131`	`131`	`/* clang-format on */`
`132`	`132`