File tree Expand file tree Collapse file tree 3 files changed +11
-2
lines changed
Expand file tree Collapse file tree 3 files changed +11
-2
lines changed Original file line number Diff line number Diff line change @@ -69,6 +69,8 @@ THE SOFTWARE.
6969#define EFFECTIVELY_USEABLE_BITS 30
7070#endif
7171
72+ #define MAX_XOR_RECOVER_SIZE 8
73+
7274#if defined _WIN32
7375 #define DLL_PUBLIC __declspec (dllexport)
7476#else
Original file line number Diff line number Diff line change @@ -954,6 +954,11 @@ void Main::parse_polarity_type()
954954
955955void Main::manually_parse_some_options ()
956956{
957+ if (conf.maxXorToFind > MAX_XOR_RECOVER_SIZE) {
958+ cout << " ERROR: The '--maxxorsize' parameter cannot be lager than " << MAX_XOR_RECOVER_SIZE << endl;
959+ exit (-1 );
960+ }
961+
957962 if (conf.shortTermHistorySize <= 0 ) {
958963 cout
959964 << " You MUST give a short term history size (\" --gluehist\" )" << endl
Original file line number Diff line number Diff line change @@ -29,6 +29,7 @@ THE SOFTWARE.
2929#include < algorithm>
3030#include < set>
3131#include < limits>
32+ #include " constants.h"
3233#include " xor.h"
3334#include " cset.h"
3435#include " watcharray.h"
@@ -63,7 +64,8 @@ class PossibleXor
6364 cout << " Trying to create XOR from clause: " << cl << endl;
6465 #endif
6566
66- assert (cl.size () <= sizeof (origCl)/sizeof (Lit));
67+ assert (cl.size () <= sizeof (origCl)/sizeof (Lit)
68+ && " The XOR being recovered is larger than MAX_XOR_RECOVER_SIZE" );
6769 for (size_t i = 0 ; i < size; i++) {
6870 origCl[i] = cl[i];
6971 if (i > 0 )
@@ -129,7 +131,7 @@ class PossibleXor
129131 // 0 1 0
130132 // 0 0 1
131133 vector<char > foundComb;
132- Lit origCl[8 ];
134+ Lit origCl[MAX_XOR_RECOVER_SIZE ];
133135 cl_abst_type abst;
134136 uint32_t size;
135137 bool rhs;
You can’t perform that action at this time.
0 commit comments