add a comment on mod_exprt

kroening · kroening · commit 2211b0367c48 · 2021-06-25T16:57:37.000+01:00
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
@@ -1044,7 +1044,10 @@ inline div_exprt &to_div_expr(exprt &expr)
 }
 
 
-/// \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
`@@ -1044,7 +1044,10 @@ inline div_exprt &to_div_expr(exprt &expr)`
`1044`	`1044`	`}`
`1045`	`1045`
`1046`	`1046`
`1047`		`-/// \brief Modulo`
	`1047`	`+/// \brief Modulo defined as lhs-(rhs * truncate(lhs/rhs)).`
	`1048`	`+/// The sign follows the lhs or dividend. This matches C99 and`
	`1049`	`+/// SMT-LIB's bvsrem but differs from the Euclidian definition`
	`1050`	`+/// and from SMT-LIB's bvsmod.`
`1048`	`1051`	`class mod_exprt:public binary_exprt`
`1049`	`1052`	`{`
`1050`	`1053`	`public:`