Extra pointer field breaks writes

[gebner]

#include "pal.h"
#include <stdint.h>

struct s {
    int *b; // adding this field breaks the function below
    int c;
};

void write(struct s *s, int x)
    _ensures(s->c == x)
{
    s->c = x;
}

Error:

* Error 19 at out/Func_write.fst(18,24-20,50):
  - Could not prove equality of:
  - Pulse.Lib.Reference.pts_to var_s
      (Struct_s.Mkstruct_s val_s_0.struct_s__b var_x)
  - Pulse.Lib.Reference.pts_to var_s val_s_0
  - Assertion failed
  - The SMT solver could not prove the query.
  - Env =
      (var_s : Pulse.Lib.Reference.ref Struct_s.struct_s)
      (var_x : FStar.Int32.t) (val_s_0 : FStar.Ghost.erased Struct_s.struct_s)
      (val_s_1 : FStar.Ghost.erased Struct_s.struct_s__spec)
      (var_s
        :
        Pulse.Lib.Reference.ref (Pulse.Lib.Reference.ref Struct_s.struct_s))
      (var_x : Pulse.Lib.Reference.ref FStar.Int32.t)
      (__anf1 : Pulse.Lib.Reference.ref Struct_s.struct_s)
      (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf1 var_s))
      (__anf0 : Pulse.Lib.Reference.ref Struct_s.struct_s)
      (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf0 var_s))
      (__anf2 : Pulse.Lib.Reference.ref FStar.Int32.t)
      (__
        :
        Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf2
              (Struct_s.struct_s__c_1 var_s))) (__anf0 : FStar.Int32.t)
      (__ : Prims.squash (Pulse.Lib.Core.rewrites_to_p __anf0 var_x))
      (__ : Prims.unit)
  - VC =
      Pulse.Lib.Reference.pts_to var_s
        (Struct_s.Mkstruct_s val_s_0.struct_s__b var_x) ==
      Pulse.Lib.Reference.pts_to var_s val_s_0
  - Also see: Func_write.fst(14,6-20,50)
  - Other related locations: Func_write.fst(14,33-20,50)

1 error was reported (see above)

[gebner]

This is an ugly workaround that works for now:

#include "pal.h"
#include <stdint.h>

struct s {
    int *b; // adding this field breaks the function below
    int c;
};

void write(struct s *s, int x)
    _ensures(s->c == x)
{
    s->c = x;
    _assert(_inline_pulse(pts_to $(s) { $field(struct s::b) = _; $field(struct s::c) = _ }));
}

[gebner]

This also works:

#include "pal.h"
#include <stdint.h>

struct s {
    int *b; // adding this field breaks the function below
    int c;
};

void write(struct s *s, int x)
    _ensures(s->c == x)
{
    s->c = x;
    _ghost_stmt($fold(struct s) $(s) _ _);
}