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

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.