daily pastebin goal
59%
SHARE
TWEET

Untitled

ereIamJH Nov 30th, 2018 106 Never
Upgrade to PRO!
ENDING IN00days00hours00mins00secs
 
  1. xxxx@xxx:~/Develop/smt$ cat arm-crkme-1.b read10str.c
  2.  
  3. (declare-const a0 (_ BitVec 32))
  4. (declare-const a1 (_ BitVec 32))
  5. (declare-const a2 (_ BitVec 32))
  6. (declare-const a3 (_ BitVec 32))
  7. (declare-const a4 (_ BitVec 32))
  8.  
  9. (assert (= #x69790439 (bvxor a0 #x12345678)))
  10. (assert (= #xc2819e87 (bvadd a0 a1)))
  11. (assert (= #xe91e0419 (bvsub a2 a1)))
  12. (assert (= #xdd1f1d1c (bvsub a2 a3)))
  13. (assert (= #xd07a8174 (bvadd a4 a3)))
  14. (check-sat)
  15.  
  16. /* quick progam to convert 1s and 0s
  17.  * output from boolector to string
  18.  */
  19.  
  20. #include <stdio.h>
  21. #include <stdlib.h>
  22.  
  23. int main(void)
  24. {
  25.     char *endptr, *line = NULL;
  26.     size_t len = 0;
  27.     ssize_t read;
  28.     long val;
  29.     long *intptr;
  30.  
  31.     // only read from stdin
  32.     while ((read = getline (&line, &len, stdin)) != -1) {
  33.  
  34.         // lop off newline
  35.         line[len-1] = 0;
  36.         // convert binary to long
  37.         val = strtol(line, &endptr, 2);
  38.         intptr = &val;
  39.         printf("%s", intptr);
  40.     }
  41.     printf("\n");
  42. }
  43. xxxx@xxx:~/Develop/smt$ boolector -m arm-crkme-1.b  | awk '{print $2}' | ./read10str
  44. ARM{FL4G_PR0C33S1NG}
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top