Skip to content

Commit 54d5ab7

Browse files
gebnerCopilot
andcommitted
Add unary minus to hauntedc parser and fix INT32_FITS macro
- Add Punct::Dash (unary minus) to the hauntedc parser's unary_expression, enabling expressions like -2147483647 in _requires/_ensures annotations - Add SpecInt case for Neg in emit_unop, emitting op_Minus - Fix INT32_FITS macro in malloc.c to use INT32_MIN properly Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent 59982f5 commit 54d5ab7

3 files changed

Lines changed: 9 additions & 2 deletions

File tree

src/hauntedc.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -709,6 +709,13 @@ fn expr_parser<
709709
.with_loc(sift.resolve_source_info(&extra.span()))
710710
.into()
711711
}),
712+
punct(Punct::Dash)
713+
.ignore_then(cast_expression.clone())
714+
.map_with(|e: Expr, extra| {
715+
ExprT::UnOp(UnOp::Neg, e.to_rvalue())
716+
.with_loc(sift.resolve_source_info(&extra.span()))
717+
.into()
718+
}),
712719
));
713720

714721
and_then!(type_name.delimited_by(punct(Punct::LParen), punct(Punct::RParen)), {

src/pass/emit.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -768,6 +768,7 @@ fn emit_unop(env: &Env, op: UnOp, ty: MaybeRc<Type>) -> Option<Doc> {
768768
let modu = get_int_mod(signed, width)?;
769769
Doc::text(format!("{}.sub {}.zero", modu, modu))
770770
}
771+
(UnOp::Neg, TypeT::SpecInt) => Doc::text("op_Minus"),
771772
(UnOp::Neg, _) => return None,
772773
(UnOp::BitNot, TypeT::Int { signed, width }) => {
773774
Doc::text(format!("{}.lognot", get_int_mod(signed, width)?))

test/malloc.c

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,7 @@ point_ptr mk_point()
2323
return p;
2424
}
2525

26-
// TODO: > INT32_MIN
27-
#define INT32_FITS(x) ((x) >= 0 && (x) < INT32_MAX)
26+
#define INT32_FITS(x) (INT32_MIN <= (x) && (x) <= INT32_MAX)
2827

2928
int sum_point(const point_ptr p)
3029
_requires(INT32_FITS((_specint) p->x + p->y))

0 commit comments

Comments
 (0)