diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index fd6e239ce..3e058f2ea 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -4423,11 +4423,21 @@ and doExp (asconst: bool) (* This expression is used as a constant *) | Lval (Var {vname= ("__builtin_nan" | "__builtin_nanf" | "__builtin_nanl" | "__builtin_nans" | "__builtin_nansf" | "__builtin_nansl"); _}, NoOffset) -> true | _ -> false in + let isSparseBuiltin = + match f'' with + | Lval (Var {vname= ("__context__"); _}, NoOffset) -> + ignore (warn "Ignoring __context__ builtin of Linux kernel Sparse"); + true + | _ -> false + in if isBuiltinNan && asconst then (* Replace call to builtin nan with computation yielding NaN *) let onef = Const(CReal(0.0,FDouble,None)) in let zerodivzero = mkCast ~kind:Internal ~e:(BinOp(Div,onef,onef,doubleType)) ~newt:resType in (empty,zerodivzero,resType) + else if isSparseBuiltin then + let one = Const(CInt(cilint_of_int 1, IInt, None)) in + (empty, one, intType) else ( (* If the "--forceRLArgEval" flag was used, make sure we evaluate args right-to-left. diff --git a/test/small1/sparse_context.c b/test/small1/sparse_context.c new file mode 100644 index 000000000..c637d7a0b --- /dev/null +++ b/test/small1/sparse_context.c @@ -0,0 +1,4 @@ +void test() { + __context__(RCU); + __context__(This, should, be, ignored); +} \ No newline at end of file