TL; DR Dipende da quali sono i tipi effettivi delle variabili. In tutti i casi, CBMC rileva un bug reale che potrebbe causare un comportamento indefinito. Ciò significa che è necessario correggere il codice anziché disattivare il messaggio in CBMC.
risposta completa:
generale: Al meglio delle mie conoscenze, CBMC non consente l'esclusione di determinate proprietà (d'altra parte, è possibile controllare solo una singola proprietà specifica utilizzando il --property bandiera). Se desideri una risposta/opinione ufficiale o una richiesta di funzionalità, ti consigliamo di postare nello CProver Support group.
(Naturalmente, si potrebbe usare __CPROVER_assume al fine di rendere CBMC escludere le tracce che conducono all'errore, ma questo sarebbe un molto, molto, molto idea male, in quanto ciò potrebbe rendere altri problemi irraggiungibile.)
Variante 1: presumo il codice sia qualcosa di simile (relative a questo: per favore, si prega di inviare indipendenti esempi e spiegare con precisione qual è il problema, è difficile da indovinare queste cose)
long nondet_long(void);
void main(void) {
long l = 0;
int c = 0;
long t = nondet_long();
long s = nondet_long();
long *b = &s;
l = (t + *b) & (0xffffffffL);
c += (l < t);
}
e si esegue
cbmc --signed-overflow-check test.c
dando un output simile a quello seguente?
CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 41 steps
simple slicing removed 3 assignments
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
792 variables, 2302 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.006s
Building error trace
Counterexample:
State 17 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 18 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 19 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 20 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 21 file test.c line 6 function main thread 0
----------------------------------------------------
t=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 22 file test.c line 6 function main thread 0
----------------------------------------------------
t=-9223372036854775808 (1000000000000000000000000000000000000000000000000000000000000000)
State 23 file test.c line 7 function main thread 0
----------------------------------------------------
s=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 24 file test.c line 7 function main thread 0
----------------------------------------------------
s=-9223372036854775807 (1000000000000000000000000000000000000000000000000000000000000001)
State 25 file test.c line 8 function main thread 0
----------------------------------------------------
b=((long int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)
State 26 file test.c line 8 function main thread 0
----------------------------------------------------
[email protected] (0000001000000000000000000000000000000000000000000000000000000000)
Violated property:
file test.c line 10 function main
arithmetic overflow on signed + in t + *b
!overflow("+", signed long int, t, *b)
VERIFICATION FAILED
Non penso che dovresti disabilitare questo controllo proprietà, anche se tu potessi. La ragione di questo è, come dici tu, che tale aggiunta può traboccare, e, integer overflow è un comportamento indefinito in C, o, come this answer alla domanda How to check integer overflow in C? bene lo mette:
[O] nce hai eseguito x + y, se è stato overflow, sei già in stato di hosed. È troppo tardi il per fare qualche controllo - il tuo programma potrebbe essersi già schiantato. Pensa allo che ti piace controllare la divisione per zero - se aspetti fino a quando la divisione è stata eseguita per controllare, è già troppo tardi.
Vedere anche Integer overflow and undefined behavior e How disastrous is integer overflow in C++?.
Quindi, questo è un bug reale e CBMC ha una buona ragione per dirlo a riguardo. Quello che dovresti fare è adattare il tuo codice in modo che non ci siano potenziali tracimazioni! La risposta di cui sopra suggerisce qualcosa di simile (ricordarsi di includere limits.h):
if ((*b > 0 && t > LONG_MAX - *b)
|| (*b < 0 && LONG_MIN < *b && t < LONG_MIN - *b)
|| (*b==LONG_MIN && t < 0))
{
/* Overflow will occur, need to do maths in a more elaborate, but safe way! */
/* ... */
}
else
{
/* No overflow, addition is safe! */
l = (t + *b) & (0xffffffffL);
/* ... */
}
Variante 2: Qui, presumo, il codice sia qualcosa di simile:
unsigned int nondet_uint(void);
void main(void) {
unsigned int l = 0;
unsigned int c = 0;
unsigned int t = nondet_uint();
unsigned int s = nondet_uint();
unsigned int *b = &s;
l = (t + *b) & (0xffffffffL);
c += (l < t);
}
e si esegue
cbmc --unsigned-overflow-check test.c
dando un'uscita simile alla seguente?
CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 42 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
519 variables, 1306 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.01s
Building error trace
Counterexample:
State 17 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 18 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 19 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 20 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 21 file test.c line 6 function main thread 0
----------------------------------------------------
t=0 (00000000000000000000000000000000)
State 22 file test.c line 6 function main thread 0
----------------------------------------------------
t=4187126263 (11111001100100100111100111110111)
State 23 file test.c line 7 function main thread 0
----------------------------------------------------
s=0 (00000000000000000000000000000000)
State 24 file test.c line 7 function main thread 0
----------------------------------------------------
s=3329066504 (11000110011011011000011000001000)
State 25 file test.c line 8 function main thread 0
----------------------------------------------------
b=((unsigned int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)
State 26 file test.c line 8 function main thread 0
----------------------------------------------------
[email protected] (0000001000000000000000000000000000000000000000000000000000000000)
Violated property:
file test.c line 10 function main
arithmetic overflow on unsigned + in t + *b
!overflow("+", unsigned int, t, *b)
VERIFICATION FAILED
Ancora, questo è un bug reale e CBMC ha una buona ragione per dirvi. Questo potrebbe essere fissato da
l = ((unsigned long)t + (unsigned long)*b) & (0xffffffffL);
c += (l < t);
che dà
CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 42 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
542 variables, 1561 clauses
SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.002s
VERIFICATION SUCCESSFUL
Variante 3: Se le cose sono come la precedente, ma avete signed int invece di unsigned int, le cose si fanno un po 'più complicato. Qui, a patto di utilizzare (scritto in modo leggermente più elaborato per vedere meglio cosa sta succedendo)
int nondet_int(void);
void main(void) {
int l = 0;
int c = 0;
int t = nondet_int();
int s = nondet_int();
long longt = (long)t;
long longs = (long)s;
long temp1 = longt + longs;
long temp2 = temp1 & (0xffffffffL);
l = temp2;
c += (l < t);
}
ed eseguire
cbmc --signed-overflow-check test.c
otterrete
CBMC version 5.1 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 48 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 3 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
872 variables, 2430 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.008s
Building error trace
Counterexample:
State 17 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 18 file test.c line 4 function main thread 0
----------------------------------------------------
l=0 (00000000000000000000000000000000)
State 19 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 20 file test.c line 5 function main thread 0
----------------------------------------------------
c=0 (00000000000000000000000000000000)
State 21 file test.c line 6 function main thread 0
----------------------------------------------------
t=0 (00000000000000000000000000000000)
State 22 file test.c line 6 function main thread 0
----------------------------------------------------
t=-2147483648 (10000000000000000000000000000000)
State 23 file test.c line 7 function main thread 0
----------------------------------------------------
s=0 (00000000000000000000000000000000)
State 24 file test.c line 7 function main thread 0
----------------------------------------------------
s=1 (00000000000000000000000000000001)
State 25 file test.c line 9 function main thread 0
----------------------------------------------------
longt=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 26 file test.c line 9 function main thread 0
----------------------------------------------------
longt=-2147483648 (1111111111111111111111111111111110000000000000000000000000000000)
State 27 file test.c line 10 function main thread 0
----------------------------------------------------
longs=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 28 file test.c line 10 function main thread 0
----------------------------------------------------
longs=1 (0000000000000000000000000000000000000000000000000000000000000001)
State 29 file test.c line 11 function main thread 0
----------------------------------------------------
temp1=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 31 file test.c line 11 function main thread 0
----------------------------------------------------
temp1=-2147483647 (1111111111111111111111111111111110000000000000000000000000000001)
State 32 file test.c line 12 function main thread 0
----------------------------------------------------
temp2=0 (0000000000000000000000000000000000000000000000000000000000000000)
State 33 file test.c line 12 function main thread 0
----------------------------------------------------
temp2=2147483649 (0000000000000000000000000000000010000000000000000000000000000001)
Violated property:
file test.c line 14 function main
arithmetic overflow on signed type conversion in (signed int)temp2
temp2 = -2147483648l
VERIFICATION FAILED
Oppure, scritte più concisamente, se si dispone di
t == -2147483648 (0b10000000000000000000000000000000)
s == 1 (0b00000000000000000000000000000001)
poi
temp2 == 2147483649 (0b0000000000000000000000000000000010000000000000000000000000000001)
e un tentativo di convertirlo in un signed int è problemi, perché è fuori intervallo (vedi anche Does cast between signed and unsigned int maintain exact bit pattern of variable in memory?).
Come si può vedere, questo controesempio è anche un bug reale e, di nuovo, CBMC ha ragione nel dirvi di questo. Ciò significa in particolare che il mascheramento/matematica non funziona come previsto (il mascheramento trasforma un numero negativo in un numero positivo che è fuori limite) ed è necessario correggere il codice, in modo che il risultato rientri nell'intervallo necessario. (Probabilmente vale la pena riflettere attentamente su ciò che effettivamente si vuole fare per assicurarsi di ottenere i risultati corretti.)