~lbnz/xr0

b84124029b8c2bddb0daaca1305f864f53bafce7 — Xr0 Team 2 months ago f4d8901 fix/bang
fix: bang operator not working

resolves: https://github.com/xr0-org/xr0/issues/43
2 files changed, 27 insertions(+), 16 deletions(-)

M src/ast/expr/verify.c
M src/value/value.c
M src/ast/expr/verify.c => src/ast/expr/verify.c +26 -16
@@ 10,6 10,7 @@
#include "math.h"
#include "object.h"
#include "props.h"
#include "stmt/stmt.h"
#include "state.h"
#include "util.h"
#include "value.h"


@@ 467,18 468,13 @@ ast_expr_eval(struct ast_expr *expr, struct state *state)
static struct result *
expr_literal_eval(struct ast_expr *expr, struct state *state)
{
	struct result *res = result_value_create(
		state_static_init(state, expr)
	);
	return res;
	return result_value_create(state_static_init(state, expr));
}

static struct result *
expr_constant_eval(struct ast_expr *expr, struct state *state)
{
	return result_value_create(
		value_int_create(ast_expr_as_constant(expr))
	);
	return result_value_create(value_int_create(ast_expr_as_constant(expr)));
}

static struct result *


@@ 532,18 528,19 @@ static struct result *
address_eval(struct ast_expr *, struct state *);

static struct result *
bang_eval(struct ast_expr *, struct state *);

static struct result *
expr_unary_eval(struct ast_expr *expr, struct state *state)
{
	struct ast_expr *operand = ast_expr_unary_operand(expr);
	switch (ast_expr_unary_op(expr)) {
	case UNARY_OP_DEREFERENCE:
		return dereference_eval(expr, state);
		return dereference_eval(operand, state);
	case UNARY_OP_ADDRESS:
		return address_eval(expr, state);
		return address_eval(operand, state);
	case UNARY_OP_BANG:
		/* XXX: hack because we stmt_exec pre as a preproces to verify
		 * constructors, this breaks any preconditions like: pre: !(p ==
		 * 0) */
		return result_value_create(value_literal_create("hack"));
		return bang_eval(operand, state);
	default:
		assert(false);
	}


@@ 558,7 555,7 @@ binary_deref_eval(struct ast_expr *expr, struct state *state);
static struct result *
dereference_eval(struct ast_expr *expr, struct state *state)
{
	struct ast_expr *binary = expr_to_binary(ast_expr_unary_operand(expr));
	struct ast_expr *binary = expr_to_binary(expr);
	struct result *res = binary_deref_eval(binary, state);
	ast_expr_destroy(binary);
	return res;


@@ 618,13 615,24 @@ binary_deref_eval(struct ast_expr *expr, struct state *state)
static struct result *
address_eval(struct ast_expr *expr, struct state *state)
{
	struct ast_expr *operand = ast_expr_unary_operand(expr);
	char *id = ast_expr_as_identifier(operand);
	char *id = ast_expr_as_identifier(expr);
	struct value *v = state_getloc(state, id);
	return result_value_create(v);
}

static struct result *
bang_eval(struct ast_expr *expr, struct state *state)
{
	struct decision dec = sel_decide(expr, state);
	if (dec.err) {
		return result_error_create(dec.err);
	}
	/* XXX */
	return result_value_create(value_int_create(dec.decision ? 0 : 1));
}


static struct result *
expr_structmember_eval(struct ast_expr *expr, struct state *s)
{
	struct ast_expr *root = ast_expr_member_root(expr);


@@ 1225,6 1233,8 @@ reduce_assume(struct ast_expr *expr, bool value, struct state *s)
	case EXPR_BINARY:
		return binary_assume(expr, value, s);
	default:
		printf("state: %s\n", state_str(s));
		printf("expr: %s\n", ast_expr_str(expr));
		assert(false);
	}
}

M src/value/value.c => src/value/value.c +1 -0
@@ 32,6 32,7 @@ struct value {
		} _struct;
	};
}; 

struct value *
value_ptr_create(struct location *loc)
{