Ho pubblicato un nuovo post (in inglese) dal titolo “Bounded model checking with CBMC and Glucose”.
Continua »

Di recente avevamo bisogno di usare un’unica variabile int per contenere due interi di piccole dimensioni. (Lasciamo perdere i dettagli e facciamo finta che int sia una variabile a 32 bit, ok?) Nulla di complicato, ma comunque ci sono voluti un paio di tentativi prima che tutto filasse liscio. Quindi, se a qualcuno servisse, ecco il codice: Il main() proverà tutte le possibili coppie, terminando con un errore se l’unpacking di una tupla porta a risultati inattesi.
Continua »