%{

/*
 *	Copyright (c) 2002 by Laboratoire Spécification et Vérification (LSV),
 *	CNRS UMR 8643 & ENS Cachan.
 *	Written by Jean Goubault-Larrecq.  Not derived from licensed software.
 *
 *	Permission is granted to anyone to use this software for any
 *	purpose on any computer system, and to redistribute it freely,
 *	subject to the following restrictions:
 *
 *	1. Neither the author nor its employer is responsible for the consequences of use of
 *		this software, no matter how awful, even if they arise
 *		from defects in it.
 *
 *	2. The origin of this software must not be misrepresented, either
 *		by explicit claim or by omission.
 *
 *	3. Altered versions must be plainly marked as such, and must not
 *		be misrepresented as being the original software.
 *
 *	4. This software is restricted to non-commercial use only.  Commercial
 *		use is subject to a specific license, obtainable from LSV.
 *		This was developed as part of the EVA project; as such, access
 *		to this software by partners of the RNTL EVA Project (Trusted
 *		Logic S.A., Verimag) is defined by the intellectual property
 *		agreement signed as part of this project.
 */

#include <stdlib.h>
#include <stdio.h>
#include <time.h>
#include <setjmp.h>
#include "yyltype.h"
#include "eva.tab.h"

extern jmp_buf errbuf;
int theSpecLineno = 1;

extern YYLTYPE yylloc; /* location data for the lookahead */
extern void *Malloc (size_t size);

static void setfilename (char *s)
{
  int len = strlen (s);

  if (yylloc.text!=NULL)
    free (yylloc.text);
  yylloc.text = Malloc (len+1);
  strcpy (yylloc.text, s);
}

#define BUMP bump();
#define BUMPCR bumpcr();

static void bump()
{
  yylloc.first_line = yylloc.last_line;
  yylloc.first_column = yylloc.last_column;
  yylloc.last_column += yyleng;
}

static void bumpcr()
{
  register char *s,*send;

  yylloc.first_line = yylloc.last_line;
  yylloc.first_column = yylloc.last_column;
  for (s=yytext, send=s+yyleng; s<send; s++)
    {
      yylloc.last_column++;
      if (*s=='\n')
	{
	  yylloc.last_line++;
	  yylloc.last_column = 0;
	}
    }
}

#define MAX_STR_CONST 5120
char string_buf[MAX_STR_CONST+1];
static char *string_buf_end = string_buf+MAX_STR_CONST;
static char *string_buf_ptr;
#define STRBUF_PUT(c) { if (string_buf_ptr>=string_buf_end) yyerr("string constant too long",""); \
			*string_buf_ptr++ = c; }

void yywarn(char *msg, char *more)
{
  fprintf (stderr, "%s%s\n", msg, more);
  fflush (stderr);
}

void yyerr(char *msg, char *more)
{
  yywarn (msg, more);
  longjmp (errbuf, 1);
}

static int yywrap (void)
{
  return 1; /* stop */
}

%}

%x COMMENT
%x STRING
%x LINE
%x LINE2

SPACE [\ \t\f]
DIG [0-9]
INT ({DIG}+)
FMT [\ \t\n\r\f]
LETTER [A-Za-z]
ALPHA [A-Za-z0-9\_]
ID ({LETTER}{ALPHA}*)

%option always-interactive
%option stack

%%

<STRING>{
  \"	{ BUMP yy_pop_state (); *string_buf_ptr = 0;
          switch (YYSTATE)
	    {
              case INITIAL: return kw_string_constant;
              case LINE: case LINE2: setfilename (string_buf); break;
            }
	   }
  \n+	{ BUMPCR theSpecLineno += yyleng; yyerr ("unterminated string constant", ""); }
  \\[0-7]{1,3}	{ /* octal escape sequence */
                   int result; BUMP
                   (void) sscanf( yytext + 1, "%o", &result );
                   if ( result > 0xff )
                     yyerr("constant out of bounds: ", yytext);
		   STRBUF_PUT(result);
                   }
  \\[0-9]+	{ BUMP yyerr("bad escape sequence: ", yytext); }
  \\n	{ BUMP STRBUF_PUT('\n'); }
  \\t	{ BUMP STRBUF_PUT('\t'); }
  \\r	{ BUMP STRBUF_PUT('\r'); }
  \\b	{ BUMP STRBUF_PUT('\b'); }
  \\f	{ BUMP STRBUF_PUT('\f'); }
  \\(.|\n)	{ BUMPCR STRBUF_PUT(yytext[1]); }
  [^\\\n\"]+	{ char *yptr = yytext; BUMP
		  while ( *yptr )
		    STRBUF_PUT(*yptr++);
                   }
  .	{ BUMP STRBUF_PUT(yytext[1]); }
  <<EOF>>	{ yyerr ("unterminated string",""); }
}

"//"[^\n]*\n+	{ BUMPCR; /* comment */ }
"/*"	{ BUMP BEGIN(COMMENT); }
<COMMENT>{
  [^*\n]*	{ BUMP /* eat anything that's not a '*' */ }
  "*"+[^*/\n]*  { BUMP /* eat up '*'s not followed by '/'s */ }
  \n+            { BUMPCR }
  "*"+"/"       { BUMP BEGIN(INITIAL); }
  <<EOF>>	{ yyerr("unterminated comment",""); }
}

{SPACE}+	BUMP
\n+	BUMPCR theSpecLineno += yyleng;
{INT}	BUMP return kw_int;
alias	BUMP return kw_alias;
assume	BUMP return kw_assume;
axiom	BUMP return kw_axiom;
basetype BUMP return kw_basetype;
case	BUMP return kw_case;
claim	BUMP return kw_claim;
everybody BUMP return kw_everybody;
hash	BUMP return kw_hash;
keypair BUMP return kw_keypair;
knows	BUMP return kw_knows;
secret  BUMP return kw_secret;
session BUMP return kw_session;
shared  BUMP return kw_shared;
switch	BUMP return kw_switch;
true	BUMP return kw_true;
false	BUMP return kw_false;
{ID}	BUMP return kw_id;
{INT}\.	BUMP return kw_label;
{ID}\.	BUMP return kw_label;
\-\>	BUMP return kw_arrow;
=\>	BUMP return kw_implies;
==	BUMP return kw_tst_equal;
:=	BUMP return kw_assign;
\&\&	BUMP return kw_and;
\|\|	BUMP return kw_or;
\*E	BUMP return kw_E;
\*A	BUMP return kw_A;
\*N	BUMP return kw_N;
\*U	BUMP return kw_U;
\*W	BUMP return kw_W;
\*S	BUMP return kw_S;
\*B	BUMP return kw_B;
\*F	BUMP return kw_F;
\*G	BUMP return kw_G;
\*P	BUMP return kw_P;
\*Q	BUMP return kw_Q;
\"	{ BUMP string_buf_ptr = string_buf; yy_push_state (STRING); }
^\#     BUMP string_buf[0] = 0; yy_push_state (LINE);
<LINE>{DIG}+   { int lineno;
             sscanf (yytext, "%d", &lineno);
	     yylloc.last_line = lineno-1;
	     BEGIN(LINE2);
           }
<LINE,LINE2>{
  {SPACE}+ BUMP
  \n       BUMPCR yy_pop_state ();
  
  \"	{ BUMP string_buf_ptr = string_buf; yy_push_state (STRING); }
  .     ;
  <<EOF>> { yyerr("unterminated line directive",""); }
}
.	BUMP return yytext[0];
<<EOF>>	{ return kw_eof; }

%%

int get_buf_pos (YY_BUFFER_STATE b)
{
  return yy_c_buf_p - b->yy_ch_buf;
}