add a comment on mod_exprt

kroening · kroening · commit 2cf541879c67 · 2021-06-25T17:01:20.000+01:00
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
@@ -1043,8 +1043,10 @@ inline div_exprt &to_div_expr(exprt &expr)
   return ret;
 }
 
-
-/// \brief Modulo
+/// \brief Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
+/// The sign follows the lhs or dividend. This matches C99 and
+/// SMT-LIB's bvsrem but differs from the Euclidian definition
+/// and from SMT-LIB's bvsmod.
 class mod_exprt:public binary_exprt
 {
 public:

Original file line number	Diff line number	Diff line change
`@@ -1043,8 +1043,10 @@ inline div_exprt &to_div_expr(exprt &expr)`
`1043`	`1043`	`return ret;`
`1044`	`1044`	`}`
`1045`	`1045`
`1046`		`-`
`1047`		`-/// \brief Modulo`
	`1046`	`+/// \brief Modulo defined as lhs-(rhs * truncate(lhs/rhs)).`
	`1047`	`+/// The sign follows the lhs or dividend. This matches C99 and`
	`1048`	`+/// SMT-LIB's bvsrem but differs from the Euclidian definition`
	`1049`	`+/// and from SMT-LIB's bvsmod.`
`1048`	`1050`	`class mod_exprt:public binary_exprt`
`1049`	`1051`	`{`
`1050`	`1052`	`public:`