diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 084eaf5880092742d59053497a923de2415ec520..70ab53fe7e64e87ae9e68af4df2a8308145dcbdc 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -6278,7 +6278,7 @@ and doExp local_env finishExp [] (se' +++ (mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid - (Set(lv, makeCastT result tresult t, + (Set(lv, snd (castTo tresult t result), CurrentLoc.get ())),[],[lv],r')) e' t @@ -6333,7 +6333,7 @@ and doExp local_env (se' +++ (mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid (Set(lv, - makeCastT opresult tresult (typeOfLval lv), + snd (castTo tresult (typeOfLval lv) opresult), CurrentLoc.get ())), [],[lv], r')) result diff --git a/tests/value/bool.i b/tests/value/bool.i index 7d1c46359f3aa59627c852379d1185abcb53567a..5a7342750bf878b8d6591770294a34e985bf3705 100644 --- a/tests/value/bool.i +++ b/tests/value/bool.i @@ -16,7 +16,17 @@ int valid_bool () { Frama_C_show_each(x, y); x=x+1; Frama_C_show_each(x); - x=x+1; + ++x; + Frama_C_show_each(x); + x++; + Frama_C_show_each(x); + x--; + Frama_C_show_each(x); + x--; + Frama_C_show_each(x); + --x; + Frama_C_show_each(x); + --x; Frama_C_show_each(x); return y; } diff --git a/tests/value/oracle/bool.res.oracle b/tests/value/oracle/bool.res.oracle index 1c1bff9d259d113886def4b86f73ddc83091f1ea..81b4e6d47d83f712f9c94bdb61fb466d10ad87ea 100644 --- a/tests/value/oracle/bool.res.oracle +++ b/tests/value/oracle/bool.res.oracle @@ -5,41 +5,46 @@ [eva:initial-state] Values of globals at initialization rand ∈ [--..--] [eva] computing for function valid_bool <- main. - Called from tests/value/bool.i:61. + Called from tests/value/bool.i:71. [eva] tests/value/bool.i:12: Frama_C_show_each: {0} [eva] tests/value/bool.i:14: Frama_C_show_each: {1} [eva] tests/value/bool.i:16: Frama_C_show_each: {1}, {2} [eva] tests/value/bool.i:18: Frama_C_show_each: {1} [eva] tests/value/bool.i:20: Frama_C_show_each: {1} +[eva] tests/value/bool.i:22: Frama_C_show_each: {1} +[eva] tests/value/bool.i:24: Frama_C_show_each: {0} +[eva] tests/value/bool.i:26: Frama_C_show_each: {1} +[eva] tests/value/bool.i:28: Frama_C_show_each: {0} +[eva] tests/value/bool.i:30: Frama_C_show_each: {1} [eva] Recording results for valid_bool [eva] Done for function valid_bool [eva] computing for function invalid_bool <- main. - Called from tests/value/bool.i:62. -[eva:alarm] tests/value/bool.i:33: Warning: + Called from tests/value/bool.i:72. +[eva:alarm] tests/value/bool.i:43: Warning: trap representation of a _Bool lvalue. assert ub.b ≡ 0 ∨ ub.b ≡ 1; -[eva] tests/value/bool.i:36: Frama_C_show_each_zero: {0} -[eva] tests/value/bool.i:39: Frama_C_show_each_one: {1} -[eva:alarm] tests/value/bool.i:42: Warning: - trap representation of a _Bool lvalue. assert ub.b ≡ 0 ∨ ub.b ≡ 1; -[eva:alarm] tests/value/bool.i:45: Warning: - trap representation of a _Bool lvalue. assert ub.b ≡ 0 ∨ ub.b ≡ 1; -[eva] tests/value/bool.i:46: Frama_C_show_each_zero_or_one: {0; 1} +[eva] tests/value/bool.i:46: Frama_C_show_each_zero: {0} [eva] tests/value/bool.i:49: Frama_C_show_each_one: {1} [eva:alarm] tests/value/bool.i:52: Warning: + trap representation of a _Bool lvalue. assert ub.b ≡ 0 ∨ ub.b ≡ 1; +[eva:alarm] tests/value/bool.i:55: Warning: + trap representation of a _Bool lvalue. assert ub.b ≡ 0 ∨ ub.b ≡ 1; +[eva] tests/value/bool.i:56: Frama_C_show_each_zero_or_one: {0; 1} +[eva] tests/value/bool.i:59: Frama_C_show_each_one: {1} +[eva:alarm] tests/value/bool.i:62: Warning: trap representation of a _Bool lvalue. assert b ≡ 0 ∨ b ≡ 1; -[eva:alarm] tests/value/bool.i:56: Warning: +[eva:alarm] tests/value/bool.i:66: Warning: trap representation of a _Bool lvalue. assert *p ≡ 0 ∨ *p ≡ 1; -[eva] tests/value/bool.i:57: Frama_C_show_each_zero_or_one: {0; 1} +[eva] tests/value/bool.i:67: Frama_C_show_each_zero_or_one: {0; 1} [eva] Recording results for invalid_bool [eva] Done for function invalid_bool [eva] Recording results for main [eva] done for function main -[eva] tests/value/bool.i:33: - assertion 'Eva,bool_value' got final status invalid. -[eva] tests/value/bool.i:42: +[eva] tests/value/bool.i:43: assertion 'Eva,bool_value' got final status invalid. [eva] tests/value/bool.i:52: assertion 'Eva,bool_value' got final status invalid. +[eva] tests/value/bool.i:62: + assertion 'Eva,bool_value' got final status invalid. [eva] ====== VALUES COMPUTED ====== [eva:final-states] Values at end of function invalid_bool: ub{.b; .c; .s[bits 0 to 7]} ∈ {0; 1}