/* Copyright 2009-2012 The MathWorks, Inc. */

#include "host_timer_x86_lcc.h"

/* With the LCC compiler, only a 32-bit timer value is supported */
uint32_T timestamp_x86_lcc(void) {
    _asm("rdtsc");
}