1 /*
2  * This file is part of the Yices SMT Solver.
3  * Copyright (C) 2018 SRI International.
4  *
5  * Yices is free software: you can redistribute it and/or modify
6  * it under the terms of the GNU General Public License as published by
7  * the Free Software Foundation, either version 3 of the License, or
8  * (at your option) any later version.
9  *
10  * Yices is distributed in the hope that it will be useful,
11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13  * GNU General Public License for more details.
14  *
15  * You should have received a copy of the GNU General Public License
16  * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
17  */
18 
19 /*
20  * YICES API EXAMPLE: OUT-OF-MEMORY CALLBACK IN C++
21  */
22 
23 #include <assert.h>
24 #include <stdio.h>
25 #include <yices.h>
26 
27 #include <new>
28 #include <iostream>
29 
30 /*
31  * Throw an exception if Yices runs out-of-memory
32  */
out_of_mem()33 static void out_of_mem() {
34   std::bad_alloc exception;
35   throw exception;
36 }
37 
main()38 int main() {
39   printf("Testing Yices %s (%s, %s)\n", yices_version,
40 	 yices_build_arch, yices_build_mode);
41 
42   yices_init();
43   yices_set_out_of_mem_callback(out_of_mem);
44 
45   /*
46    * Allocate new contexts until we run out of memory.
47    * It's a good idea to set a memory limit before calling this program.
48    */
49   int n = 0;
50   while (true) {
51     n ++;
52     try {
53       yices_new_context(NULL);
54     } catch (std::bad_alloc &ba) {
55       std::cerr << "Out of Memory: " << ba.what() << " after " << n << " rounds\n";
56       return 1;
57     }
58   }
59 
60   yices_exit();
61 
62   return 0;
63 }
64